|
__NOTOC__ Temporal logic of actions (TLA) is a logic developed by Leslie Lamport, which combines temporal logic with a logic of actions. It is used to describe behaviours of concurrent systems. == Details == Statements in temporal logic are of the form , where ''A'' is an action and ''t'' contains a subset of the variables appearing in ''A''. An action is an expression containing primed and non-primed variables, such as . The meaning of the non-primed variables is ''the variable's value in this state''. The meaning of primed variables is ''the variable's value in the next state''. The above expression means the value of ''x'' ''today'', plus the value of ''x'' ''tomorrow'' times the value of y ''today'', equals the value of ''y'' ''tomorrow''. The meaning of is that either A is valid now, or the variables appearing in t do not change. This allows for stuttering steps, in which none of the program variables change their values. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「temporal logic of actions」の詳細全文を読む スポンサード リンク
|